The Cantor–Schroeder–Bernstein theorem says that the usual order relation on cardinalities of sets is antisymmetric. In other words, define an order on sets by if there exists a monomorphism . Then, if both and , there exists an isomorphism of sets .
The result is really only interesting in the absence of the axiom of choice (). With , it is a trivial corollary of the well-ordering theorem. However, the theorem actually requires only excluded middle, although it does not hold in constructive mathematics — indeed, it is actually equivalent to excluded middle (at least assuming the axiom of infinity).
We prove that the Cantor–Schroeder–Bernstein theorem holds in a Boolean topos. The theorem is not however intuitionistically valid, in that it fails in some toposes, such as the topos (the arrow category of ); see Example below.
Throughout we use ordinary set-theoretic reasoning which can be translated into the formal theory of toposes. (This can be formalized via the Mitchell–Benabou language, for instance.)
First, let’s try a little pedagogy. Somehow functions are to be cooked up from injections and , so we might guess is to be defined as at least part of the time, and as another part of the time. An ideal situation would be to have a set-up
where are complementary subsets in and are complementary subsets in ; then could be defined as on and as on , and everything works out fine. How can we achieve this?
If we have this situation, then apparently (the direct image of ), and (the complement of ), and then , and finally are required to be complementary, so we would need
In other words, would be a fixed point of a suitable operation built from direct image and complementation operators. In fact, if we find such a fixed point , then the plan above would work without a hitch.
Perhaps the simplest fixed-point theorem for this purpose on the market is
Let be an order-preserving map. Then there exists in for which .
Let be the (internal) intersection of . Since for every in , we have for every in . Hence by definition of . Applying again, we get . Hence belongs to . But then by definition of .
The preceding proof is valid in any topos (and so holds for even intuitionistically). It can be seen as a specialization to posets of a result of Lambek on the initial algebra of an endofunctor, saying that the structure maps of such initial algebras are necessarily isomorphisms. Here the initial algebra is (by construction) an initial fixed point.
Suppose given two monos , . Let denote direct image or existential quantification along , and let denote negation. Then the composite
is order-preserving, and so has a fixed point by the Knaster-Tarski lemma. Now define by the rule
(the multi-line definition is where we use the Boolean condition). The second line makes sense because is in the image of . The inverse of is
That is inverse to uses the fact that . The rest is obvious.
This classic proof is substantially the proof given in Johnstone’s Elephant, D4.1.11. The Boolean condition is not strictly speaking necessary, i.e., the principle of excluded middle () does not logically follow from the Cantor–Schroeder–Bernstein statement since, for example, using notation as above, monic endomorphisms like and are isomorphisms in
but this is a non-Boolean, non-Grothendieck topos provided that is any finite category that is not a groupoid, e.g., . But that being said, is certainly the most natural supposition to make. In fact EM does constructively follow from the Cantor-Schroeder-Bernstein statement provided that a natural numbers object exists (for instance in a Grothendieck topos); see Pradic and Brown, 2019. A proof that in a topos CSB+NNO implies Booleanness is outlined in Freyd 1994, using the stronger hypothesis that the monomorphisms have retractions.
In some schools of thought, the proof using the Knaster-Tarski lemma would be criticized because that lemma makes use of an impredicative construction. However, the application made of it in the proof of the CSB theorem is only to ensure that the operator has a fixed point. This objection can be countered by shopping around for a different fixed-point theorem, one which is predicatively and constructively valid.
A time-honored way of constructing a fixed point of an operator is by taking a limit of a sequence of iterates of that converges, provided that preserves the limit. To this end, we find that specializing Adámek’s theorem (see initial algebra of an endofunctor) suits our purposes perfectly.
If is monic, then the operator preserves limits of inverse chains (i.e. intersections of decreasing sequences).
More generally, preserves connected limits, because it lifts through the inclusion to an isomorphism (here denotes the top element of , aka ), and preserves connected limits.
In more detail: by Frobenius reciprocity, we have for elements of and of . Putting , we get , and so the composite
is the identity. But since is monic, is also the identity, which completes the proof.
preserves colimits of -chains.
Naturally the left adjoint also preserves such colimits. So by the corollary, the composite preserves colimits of -chains.
Putting now (the bottom element of ), , and generally
we have (apply the monotone operator to the inclusion ), and so preserves the union of the chain ,
which implies that is a fixed point of , as desired. In fact this is the minimal fixed point, just as in the conclusion of the Knaster-Tarski lemma. (Cf. initial algebra of an endofunctor, especially Adámek’s theorem.)
The preceding proofs are sometimes considered too abstract to easily visualize, but this is slightly misleading: the second proof, involving the construction of a minimal fixed point as a countable limit, can be “beta-reduced” to produce one of the standard “concrete” proofs.
In a nutshell, the minimal fixed point of the operator can be expressed as an alternating series of iterated direct images:
where stands for set-theoretic difference and stands for the union . The meaning of the infinite series is that we have a increasing sequence of those finite alternating sums with an even number of terms, starting with the empty sum (which is , the empty set):
etc., and the infinite series is interpreted as the countable union of this increasing sequence. Note that we have to be careful about the order of the appearance of and , but alternatively, letting be the addition in the Boolean ring (symmetric difference), we could write also the series as in the ring, where we do not need to be fussy about order.
Most of this is a routine calculation, which for the most part boils down to the following observation:
If are elements of , with , then . (With a similar statement for .)
The proof is left to the reader, but in brief, the injectivity of implies that preserves binary intersections and relative complements.
From here, if we write
then it is easily verified by induction that, referring to equation (1),
Thus, according to equation (2), the minimal fixed point is the union of the which is how we are interpreting the series (3).
Now we set up a comparison with one of the standard proofs involving a back-and-forth argument, say the one given in Wikipedia that is attributed to Julius König. The minimal fixed point is a union of finitary approximations
etc. Elements in are those which have no inverse images under . Elements in are elements in to which can be applied at most once before we hit an element of with no inverse image under . Elements in the union are those which survive at most finitely many applications of before hitting an element of with no inverse image under . In the terminology of the Wikipedia article, such elements in are called “-stoppers”, and these are exactly the elements for which (where recall is the bijection under construction) is defined to be in the Wikipedia article. For elements not in this fixed point (the non--stoppers), our proof of CSB (via a minimal fixed point) defined to be , the same prescription that is used in the Wikipedia article.
Other prescriptions are possible. For example, one could dually construct a maximal fixed point of the operator , using Lemma to note that and the right adjoint preserve limits of inverse -chains, so that the maximal fixed point or terminal algebra of the endofunctor could be constructed as an intersection . This could also be written as a series
except this time the series is interpreted as an intersection of a decreasing sequence whose partial sums have an odd number of terms:
etc. The difference between this and the minimal fixed point is the set , consisting of elements of that belong to a doubly infinite sequence or a cyclic sequence (in the terminology of the Wikipedia article). As remarked in that article, for such we have an option to define as or ; in the present article we defined for all belonging to whichever fixed point is used, which includes points in doubly infinite sequences or cyclic sequences if is the maximal fixed point. In that case the remaining (belonging to the complement of the maximal fixed point) are mapped to .
Counterexample below shows that the CSB theorem fails in Brouwer's intuitionistic mathematics even for (since every function between the sets and must be continuous by Brouwer's continuity principle!). See also the discussion in Mac Lane-Moerdijk, VI.9, on toposes that realize Brouwer’s theorem.
As mentioned above, the Cantor-Schroeder-Bernstein theorem fails in the arrow category , whose objects are functions between sets and whose morphisms are commutative squares. For example, let be the object that takes to , where is the greatest integer less than or equal to ; let be the object that takes to , where is the least integer greater than or equal to . Pretty clearly and are non-isomorphic, because has cardinality whereas all fibers of have cardinality . But, just by drawing pictures of these objects, it is easy to construct monomophisms and (e.g., define and for all , and define for , , and for all ).
Nor can one have internal existence of an isomorphism between and in this last example, since internal existence implies external existence as soon as the terminal object is (externally) projective.
In fact, the CSB theorem is equivalent in constructive mathematics (with the axiom of infinity) to the law of excluded middle. This was shown in Pradic and Brown, 2019 using the principle of omniscience for the extended natural numbers.
The CSB property holds in some other categories of interest (but arguably fails in many more). Some examples follow:
The CSB property holds in the category of Archimedean ordered fields and ring homomorphisms. This is because every Archimedean ordered field is a subset of the real numbers, and ring homomorphisms between Archimedean ordered fields are subset inclusions in the powerset of the real numbers; i.e. the category of Archimedean ordered fields is a full subcategory of the powerset of the real numbers. This remains true in constructive mathematics but one has to use the Dedekind real numbers as only the Dedekind real numbers are the terminal object in the category of Archimedean ordered fields and ring homomorphisms.
More generally, the CSB property holds in any partial order (i.e. thin gaunt category).
The CSB property holds in the category of vector spaces and in the category of algebraically closed fields. See also this MO post by John Goodrick, where model-theoretic criteria come into play, sometimes under strengthenings of the notion of monomorphism (e.g., elementary embedding, split monomorphism) Some slides by Goodrick here go into more detail, giving connections between CSB and stable theories in the sense of Shelah.
On the other hand, the CSB property obviously fails in Top, since we have embeddings , yet . It fails in Grp (e.g., the free group on countably many generators embeds in the free group on two generators).
More examples and discussion can be found at this Secret Blogging Seminar post.
In a celebrated work, Timothy Gowers gave a negative solution in the case of Banach spaces.
Martin Escardó has announced a proof of CSB in the base theory of Martin-Löf dependent type theory with the added assumption of function extensionality and excluded middle, and supplied an Agda proof (Escardó 2020). There is a slight subtlety in that “injection” is replaced by “embedding”, where the latter is defined to be a map whose fibres are subsingletons. This implies that CSB holds for homotopy types/-groupoids.
The CSB theorem was first stated by Georg Cantor, but his proof relied on the well-ordering theorem. The modern (choice-free) theorem was proved (independently) by Felix Bernstein? and Ernst Schröder?. It has been variously named after two or three of these in almost every possible combination, although Cantor (when mentioned at all) seems always to be mentioned first.
Richard Dedekind wrote out a proof on 11th July 1887, and only later published in his Nachlass in 1932 (Dedekind 1932), while working on a draft of Was sind und was sollen die Zahlen?, well before any announced proofs by Cantor, Schroeder, or Bernstein in 1895, 1896, 1897 respectively.
Richard Dedekind (1932), Robert Fricke?; Emmy Noether; Øystein Ore (eds.), Gesammelte mathematische Werke, vol. 3, Braunschweig: Friedr. Vieweg & Sohn, pp. 447–449 (Ch.62) Göttinger Digitalisierungszentrum
Peter Johnstone, Sketches of an Elephant: A Topos Theory Conpendium, Vol. I, Clarendon Press, Oxford (2002)
Timothy Gowers, A Solution to the Schroeder-Bernstein Problem for Banach Spaces, Bulletin of the London Mathematical Society, Volume 28, Issue 3 (1996), 297-304 (abstract)
Saunders Mac Lane, Ieke Moerdijk, Sheaves in Geometry and Logic, Springer-Verlag 1992.
Peter Freyd, Cantor-Bernstein - message to the category theory mailing list, February 1994. (link)
Pierre Pradic, Chad E. Brown, Cantor-Bernstein implies Excluded Middle, 2019 (arxiv:1904.09193)
Martín Hötzel Escardó, The Cantor-Schröder-Bernstein Theorem for ∞-groupoids, 2020 (blog post, Agda proof, arXiv:2002.07079)
Last revised on July 12, 2024 at 04:46:50. See the history of this page for a list of all contributions to it.